Nuprl Lemma : islocal_wf
11,40
postcript
pdf
k
:Knd. islocal(
k
)
latex
Definitions
x
:
A
.
B
(
x
)
,
Knd
,
t
T
,
islocal(
k
)
Lemmas
bnot
wf
,
isl
wf
,
IdLnk
wf
,
Id
wf
origin
k:Knd. islocal(k) 
k:Knd. islocal(k) x:A. B(x) T